This invention relates generally to information-flow downgraders and, more specifically, relates to verifying information-flow downgraders.
The information-flow security principle establishes that no “illicit flow” of information should be allowed in a program. A flow is illicit if the flow allows untrusted information to be used in a trusted computation (an integrity violation) or if the flow allows secret information to be entirely or partly revealed to unauthorized users (a confidentiality violation). Integrity and confidentiality can be seen as dual problems by simply stating that there should not be any flow of information from “high” to “low”, where “high” means “untrusted” in integrity and “secret” in confidentiality, and low means “trusted” in integrity and “public” in confidentiality. See FIG. 1, which shows a table of information flows for integrity and confidentiality and downgrading types for the same.
Information can be tagged with information-flow labels. Typically, information-flow labels form a partially ordered set or even a lattice. If information-flow security was strictly enforced and no illicit flows of information were allowed, most programs would not work. To be information-flow secure, a program would have to be “partitioned” so that information tagged with a certain label (e.g., “label 1”) can only flow to program points that have been tagged with labels higher than 1 (one). A program with these restrictions is very unlikely to be useful. For example, from an integrity point of view, a Web application is supposed to accept inputs from potentially untrusted users and use those inputs in trusted computation. As another example, an online banking program takes as input the account number and the password of a user (potentially untrusted information) and passes them to a backend database system where the account number and password are used in a trusted setting. Similarly, an online bookstore takes as input the user identification (ID) and password of the customer and the title of the book that the customer wants to buy (all potentially untrusted information), and uses them to complete a transaction.
From a confidentiality point of view, a Web application often releases data that has been computed based on secret information and, as such, should be considered secret as well: a banking application may reveal to any teller the last four digits of the social security number of any user; and an online bookstore may reveal to any shop assistant the last four digits of any customer's credit card number. Given that all these programs exhibit flows that allow “high” information to flow to “low” program points, all these programs would be rejected if information-flow security were simply enforced. To allow these programs to function, “high” information can be “downgraded” and become “low” enough to be used in “low” program points. Downgrading translates itself into “endorsement” in integrity and “declassification” in confidentiality (see FIG. 1). For example, once a program has verified that the user-provided input to a Web application is a properly formatted string, the program can endorse that input, which now becomes trusted enough to be used in a trusted computation. Similarly, once a program has verified that the information extracted from a secret is not sufficient to reveal the secret itself, the program can declassify the extracted information, which now can become public enough to be revealed to a public listener.
The part of the program that performs the downgrading is called an information-flow downgrader. A program can implement many information-flow downgraders and often there is no guarantee that a downgrader has been correctly implemented.